T:Type, L:(T List). (L = [])  (x:T. (x  L)) 

latex

Definitions

t  T, s = t, x:AB(x), x:A. B(x), (x  l), A, , Type, type List, P  Q, P  Q, A List, [car / cdr], Void, False, x:A  B(x), P & Q, P  Q, [], tl(l), n - m, if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n+m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A  B, , {x:A| B(x)} , , {T}, True, T, P  Q

Lemmas

cons member, rev implies wf, squash wf, true wf, nil member, false wf, iff wf, not wf, l member wf